Nuprl Lemma : length_of_null_list
2,24
postcript
pdf
A
:Type,
as
:
A
List.
as
= nil
||
as
|| = 0
latex
Definitions
t
T
,
Prop
,
x
:
A
.
B
(
x
)
,
||
as
||
,
P
Q
Lemmas
length
wf1
origin
A:Type, as:A List. as = nil 
||as|| = 0 A:Type, as:A List. as = nil ||as|| = 0 
Tx:A. B(x) Q